Talk:Rayo's number
Archive 1 In the archive 1 someone propose "Omega^DEF_1" as the growth rate of Rayo(n). Can someone please explain me what is this ordinal? I didn't find anything about it :/ Fluoroantimonic Acid (talk) 11:06, June 13, 2015 (UTC) :This ordinal was defined as "the least ordinal undefinable in formal system here", but the community came to the conclusion that it causes too much confusion, as this lead to many people thinking there exists the least undefinable ordinal, which is paradoxical concept. LittlePeng9 (talk) 11:11, June 13, 2015 (UTC) :Ok, thanks Fluoroantimonic Acid (talk) 11:20, June 13, 2015 (UTC) ::The main reason it was removed is because it wasn't from any source. -- ve 15:58, August 3, 2015 (UTC) Fun fact: Rayo(n) and FOST(n) aren't exactly the same, because for Rayo(n) you don't directly have access to all FOST's alphabet (e.g. you can't use the "implies" symbol directly). Of course you don't really need these, Rayo's microlanguage has everything it needs, but it costs a little more symbols, so FOST(n) will often be a very, very little bigger than Rayo(n) for the same n. I would say that Rayo(n) < FOST(n) < Rayo(2*n) Fluoroantimonic Acid (talk) 13:19, August 3, 2015 (UTC) :I don't see how the definition of Rayo(n) allows use of the "implies" symbol. The definition of Sat clearly states what operators are allowed: ∈ = ¬ ∧ ∃. -- ve 15:58, August 3, 2015 (UTC) ::I think what he is saying is precisely that Rayo(n) doesn't allow it, but "implies" is part of FOST, so FOST(n) would have to allow it. LittlePeng9 (talk) 16:17, August 3, 2015 (UTC) :::I don't see how "implies" is part of FOST either, if we have no precise definition of FOST at hand aside from Rayo's. I can argue that ordinal addition is a valid FOST operator since it can be defined in FOST. -- ve 18:08, August 3, 2015 (UTC) ::::Did Rayo said the name "FOST"? Just wanna know. Also, I consider that as a first-order language it inherits all symbols of the first-order logic "framework" Fluoroantimonic Acid (talk) 16:46, August 10, 2015 (UTC) "the smallest natural number that cannot be uniquely identified by a FOST expression of at most n symbols" The article says this is a trivial variation on Rayo's function. However, wouldn't this be much, much weaker, as Rayo's function cannot express all integers up to Rayo's number. This should be an approximately exponential growth rate, hardly uncomputable. Am I misunderstanding something? Maybe called Googology Noob (talk) 14:16, January 11, 2016 (UTC) :Fixed. Thanks. -- ve 00:40, January 12, 2016 (UTC) Better Bounds Did you know about Rayo(10^100) > 3.333E98? AarexWikia04 - 22:58, August 1, 2016 (UTC) Really? Then how do we know it is more powerful than BB(10^100) for example? Or is it just that it grows quite slowly? Mush9 (talk) 20:58, November 20, 2016 (UTC) :Aarex's comment is like saying that Graham's number is bigger than 10^40. This is without a doubt true, but Graham's number is far larger than 10^40. Similarly, Rayo(10^100) is far larger than 3.333E98. As for how we know it is larger than BB(10^100), the idea is that we can define Turing machines and Busy Beaver function is relatively small number of characters (at most a few tens of thousands, I'd believe) and we can in FOST the number BB(10^101) in not many more characters. LittlePeng9 (talk) 21:49, November 20, 2016 (UTC) Axioms of FOST Formal system consists of symbols, grammer, axioms and inference rules. FOST defines symbols, grammer, logical axioms and inference rules in the first order logic. However, non-logical axioms are not explicitly declared. As the domain of discourse of FOST is a von Neumann universe, it is natural to assume that FOST uses ZFC. Is it correct? Then if we use ZFC + "there exists I0 cardinal", we have FOST-I0. FOST-I0 should be stronger than FOST, but how strong is it? Can we also make similar extention to FOOT? �� Fish fish fish ... �� 20:36, August 9, 2016 (UTC) :If you want axioms to be relevant, you must be talking about what can be can be proven from those axioms - something like ZFC(n) = "the largest natural number m such that there is a FOST sentence phi of length n or less such that ZFC proves that m is the unique natural number to satisfy phi", or something similar. Such a function cannot significantly outgrow the Busy Beaver function: For each sentence phi, one can define a Turing machine that searches through all ZFC proofs and all m for a proof that phi is uniquely satisfied by m. Then with an oracle for the BB function (and therefore the halting function), we can define an oracle Turing machine that runs through the finitely many phi of n characters or less, picks out the ones that have ZFC proofs that phi is satisfied by some natural number, and finds the largest such natural number - this is ZFC(n). :So, to get significantly beyond the Busy Beaver function, we must abandoned provability in a recursively enumerable theory, and talk about truth in a particular model. For Rayo's function, we take the von Neumann universe V, and use FOST as the language of choice (as opposed to formal theory, which includes axioms that we are not worried about). Of course, to believe this works, we must be sufficiently Platonic to believe that V is well-specified. Deedlit11 (talk) 07:36, August 10, 2016 (UTC) ::Oh, I see. I've been thinking that FOST is a kind of first-order logic, but actually it isn't, because it doesn't have axioms. As it is explained in the main text that FOST is a first-order logic, I will note in the text that FOST doesn't include axioms. �� Fish fish fish ... �� 11:25, August 10, 2016 (UTC) ::: I do not know about the axioms of FOST. AarexWikia04 - 11:54, August 10, 2016 (UTC) :: No, but basic functions like ZFC(n) = "The largest number F(n) such that there is a proof from the ZFC axioms that is Rayo-nameable in n symbols and proves that F is total" do work, and easily outgrow all functions provably total in ZFC, such as the Busy Beaver function, and oracles, diagonalised oracles, etc. In fact, T(n) = "The largest number F(n) such that there is a proof from consistent theory that extends T and whose axioms not in T are collectively Rayo-nameable in n symbols that is Rayo-nameable in n symbols and proves that F is total" is even faster growing, and all we need to do is have T be strong enough to talk about finite ordinals (e.g. general set theory), and it beats all functions provably recursive in any extension of T with only finitely many extra axioms. Notably, this includes ZFC as we can finitely axiomise it with the one-sorted variant of NBG, and even ZFC + "There exists a strongly compact cardinal," as the latter is a first-order large cardinal axiom. ~εmli 23:03, August 14, 2016 (UTC) :::Hmm, I suppose you are saying that ZFC proves the Busy Beaver function total because one can argue that there are some finite number of Turing machines that halt, and we are simply taking the maximum score of all such machines. In a similar sense, for any fast-growing function f whatsoever, we can define g(n) = f(n) if f(n) is defined, and g(n) = 0 otherwise; then ZFC (or presumably much weaker) will prove that g(n) is total, and if f(n) is total (with or without a proof) then g(n) = f(n). :::But, I don't see how this is a "fix" for Rayo's function; the issue was that no r.e. consistent formal theory determined Rayo's function for all n, but the same is true for your ZFC(n). Yes, proofs are involved in the definition of ZFC(n), but that seems like a red herring. Deedlit11 (talk) 00:47, August 15, 2016 (UTC) :::: I disagree, as the proofs involved for the totality of the above ZFC function do not require selecting a specific model, whereas they do for Rayo's function. If what you say is the issue at hand, then I am solving a different problem. ~εmli 14:48, August 15, 2016 (UTC) Rayo's number isn't defined Quoting a recent xkcd post: Rayo's number is undefined. (Rayo's function is too, and basic extensions like Big Foot.) For the values of Rayo's number to be defined, you have to work in a specific model (a specific set of first order axioms, which could be a rectification to the system, is not sufficient). For a simple example, suppose that we work in ZFC, and \(\beth_1 = \aleph_n\) is independent of ZFC (proven, but we might be working in an extension) for each n, and the formula which is true for only n requires k symbols (k is likely only a few thousand). Now, as this value is an upper bound for Rayo(k), suppose n, in the model we work in, is larger than that. Contradiction. Note that we've already proven that n is idependent, so either we assume that we can only go off provability in theory, which is both weak (enumerate all proofs in the theory, assuming Rayo(n) is well defined) and dependent on the theory, or choose a model, which requires choosing a model based on a system where we have no axioms to go off of, which is completely arbitrary. We can, of course, go one further by noting that the definition of a "natural number" may fail in a non-well founded theory and not fail in a well-founded one. Also, it is quite well known that all first-order theories that have an infinite model have infinitely many (at least one of each infinite cardinality), so even if we added restrictions so that we also have to make an axiomatic system, the idea (at the least, for first-order theories) is failed from the get-go. Edited to add: Going back to the main point, for Rayo's function to be total, it needs to work in a system of absolute truths, as otherwise there exist sufficiently long formulas (length k and above) which may evaluate to any n (as the result is independent from the system), and this n may be larger than Rayo(k), making Rayo's function undefined for the values >=k. No such system of absolute truths can be formulated in first order logic excepting very basic ones: we either need a complete and consistent axiom system (which we can't have*, due to Gödel's incompleteness theorem), or a theory with a single model (which we can't have**, due to the Löwenheim–Skolem theorem). If I had to suggest how to "fix" the function, I would say that R(n) is the largest number F(n), such that F can be proven total in a finitely-axiomisable (one-sorted) first-order theory which can be described with at most n symbols the way Rayo used. This function grows faster than any function provably total in ZFC (using a finite axiomisation of the one-sorted variant of NBG), however this might not be the case for stronger theories or second-order theories. *Unless the theory is very weak i.e. it does not incorporate Robinson Arithmetic. **As the model must be infinite for our purposes, presumably. It may be possible to measure the size of very large finite models, however this does not seem to hold much promise, and better methods definitely exist. ~εmli 23:03, August 14, 2016 (UTC) :What you write is true; see my post in the section before this one. Rayo's number is meant to be defined for a specific model, namely the von Neumann universe V. If you take the position that truth in V is ambiguous, then Rayo's number will be undefined, as will BIG FOOT. It seems likely that Rayo is a Platonist; I know from talking with Wojowu that he (Wojowu) is quite Platonist. So for them their functions are well-defined, for many others they will not be. :Note that even the Busy Beaver function has this same problem; for any recursively enumerable consistent theory T, T cannot determine the Busy Beaver function beyond a particular point, which means there are models of the theory T which differ on the Busy Beaver function past a certain point. Deedlit11 (talk) 23:04, August 14, 2016 (UTC) :: I would say that the busy beaver function doesn't have the same problem: it is everywhere defined (easily), and the truth of such depends on the theory; models don't come into the question. Rayo's function, on the other hand, cannot be proven within the theory without talking about the models, and if we merely restrict our knowledge to a theory, then (unlike BB) we can draw contradictions like shown above. ~εmli 14:48, August 15, 2016 (UTC) Values Has anyone tried to get the first several values of Rayo's function? Rayo(1), Rayo(2), etc.? Well, the first few values don't exist, as the first valid definition of a number is (¬∃2(2∈1)), which defines 0. So Rayo(n) doesn't exist for n<=9, and Rayo(10)=0. I think after that the next few values are also 0. Tomtom2357 (talk) 08:39, October 3, 2016 (UTC) :As Rayo(n) is defined as "the smallest nonnegative integer" greater than ..., Rayo(0)=0, because it is the smallest nonnegative integer. �� Fish fish fish ... �� 04:13, October 4, 2016 (UTC) Rayo's ordinal Let's define \(\alpha\) to be the first \(\alpha\) so that \(f_\alpha(n) = \text{a good idea for a chewing gum flavor}\). Now I define first few terms of \(\alphan\): \(\alpha0 = \text{brotastic strawberries}\) \(\alpha1 = \text{awesome bananas} \) \(\alpha2 = \text{max coolality fresh mint}\) \(\alpha3 = \text{mango boost} \) \(\alpha4 = \text{fruity twirl} \) \(\alpha5 = \text{tutti frutti} \) \(\alpha6 = \text{rolling fudge}\) \(\alpha7 = \text{flavor cascade}\) \(\alpha8 = \text{warped berries}\) \(\alpha9 = \text{mint spearmint coolmint}\) \(\alpha10 = \text{Cola licious}\) \(\alpha11 = \text{Blueberry Bubblefest}\) \(\alpha12 = \text{Sour Sweet Symphony}\) \(\alpha13 = \text{Creme de le cream}\) \(\alpha14 = \text{Chocolate earth} \) \(\alpha15 = \text{Red berry mist}\) Can anyone please define other terms of fundamental sequence of \(\alpha\)? Or replace my terms with some other cool terms? 13:58, November 18, 2016 (UTC) :\(\alpha\) is not well-defined. Also, whatever \(\alpha\) would be, specifying 16 completely arbitrary ordinals doesn't specify the fundamental sequence in the slightest. \(\alpha\), as long as it's limit, will have infinitely many fundamental sequences, yet you have made no progress towards specifying any single one. But since I know the community here at least a little, I suppose Aarex will come and and help you with this helpless task. LittlePeng9 (talk) 14:14, November 18, 2016 (UTC) :''' '''Replaced the whole thing with cooler terms Chronolegends (talk) 18:28, November 18, 2016 (UTC) ::Replaced the whole thing with cooler commands. LittlePeng9 (talk) 20:04, November 18, 2016 (UTC) How is it so strong? How does the Rayo's function go beyond other uncomputable functions like the busy beaver function and xi function? —Preceding unsigned comment added by 172.58.104.162 (talk • ) 18:27, November 19, 2016 (UTC) :The basic idea is that you can define TMs and SKIO calculus in set theory (doing so is tedious, but possible). You can then iterate them and what not. LittlePeng9 (talk) 19:23, November 19, 2016 (UTC) ::LittlePeng9 do you happen to know any webpages that have turing machines being defined and iterated by set theory? If you do then could you post those weblinks, so i could visit those webpages? :::Wikipedia has a formal definition of Turing machines, but you seem to be asking about a definition in the language of set theory. I doubt anyone has ever done that, since it is an extremely tedious thing to do. The closest thing I can direct you to is this post, in which a description in a semi-formal language is given. Also, I give a description of a description (sic) of a specific Turing machine in FOST here. :::As for iterating, what I meant is given a function f(n) defined in FOST (presumably as a set of ordered pairs), you can also define in FOST the function f(f(n)) (for example), and having done this for f=BB you beat BB(n). Calling this set of ordered tuples F, you can define f(f(n)) as a set of ordered tuples FF using (borrowing notation from here): :::\((x,y)\in FF\Leftrightarrow\exists A,B,z:x=\mathrm{car}(A)\land z = \mathrm{cdr}(A)\land z = \mathrm{car}(B)\land y = \mathrm{cdr}(B)\land A\in F\land B\in F\). LittlePeng9 (talk) 20:37, November 20, 2016 (UTC) ::::What if I don't understand formal definitions? 20:44, November 20, 2016 (UTC) :::::Then that's your problem. Writing an informal definition into FOST is not possible without formalizing it. LittlePeng9 (talk) 21:43, November 20, 2016 (UTC) ::::::Okay thanks.